Nuprl Lemma : comp_nat_ind_a
12,41
postcript
pdf
P
:(
{k}). (
i
:
. (
j
:
. (
j
<
i
)
P
(
j
))
P
(
i
))
{
i
:
.
P
(
i
)}
latex
ProofTree
Definitions
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
False
,
A
,
A
B
,
,
x
.
t
(
x
)
,
Lemmas
nat
wf
,
le
wf
,
nat
plus
wf
,
nat
ind
a
origin
P:(
{k}). (i:. (j:. (j < i) 
P(j)) P(i)) {i:. P(i)}
P:({k}). (i:. (j:. (j < i) P(j)) P(i)) {i:. P(i)}
T Qx:A. B(x)
A
B
x. t(x)